not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))
AND(x, or(y, z)) → AND(x, y)
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
AND(or(y, z), x) → AND(x, y)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
AND(or(y, z), x) → AND(x, z)
AND(x, or(y, z)) → AND(x, z)
NOT(or(x, y)) → NOT(y)
not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AND(x, or(y, z)) → AND(x, y)
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
AND(or(y, z), x) → AND(x, y)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → AND(not(x), not(y))
AND(or(y, z), x) → AND(x, z)
AND(x, or(y, z)) → AND(x, z)
NOT(or(x, y)) → NOT(y)
not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
AND(x, or(y, z)) → AND(x, y)
AND(or(y, z), x) → AND(x, y)
AND(or(y, z), x) → AND(x, z)
AND(x, or(y, z)) → AND(x, z)
not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AND(x, or(y, z)) → AND(x, y)
AND(or(y, z), x) → AND(x, y)
AND(or(y, z), x) → AND(x, z)
AND(x, or(y, z)) → AND(x, z)
The value of delta used in the strict ordering is 1/8.
POL(AND(x1, x2)) = (1/2)x_1 + x_2
POL(or(x1, x2)) = 1/4 + (2)x_1 + (4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
NOT(and(x, y)) → NOT(y)
NOT(or(x, y)) → NOT(x)
NOT(and(x, y)) → NOT(x)
NOT(or(x, y)) → NOT(y)
The value of delta used in the strict ordering is 1/16.
POL(NOT(x1)) = (1/4)x_1
POL(or(x1, x2)) = 1/4 + (4)x_1 + (4)x_2
POL(and(x1, x2)) = 4 + x_1 + x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
not(not(x)) → x
not(or(x, y)) → and(not(x), not(y))
not(and(x, y)) → or(not(x), not(y))
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(or(y, z), x) → or(and(x, y), and(x, z))